During the last decade, code inspection for standard programming errors has largely been automated with static code analysis. Commercially available static program analysis tools are now routinely used in many software development organizations. These tools are popular because they find many (real) software bugs, thanks to three main ingredients: they are automatic, they are scalable, and they check many properties. In general, a tool that is able to check automatically (with sufficient precision) millions of lines of code against hundreds of coding rules and properties is bound to find on average about one bug (i.e., code error) every thousand lines of code.
As basic code inspection can be achieved using automated code analysis, cost, as part of the software development process, is typically reasonable and manageable. However, a more thorough type of testing, referred to as “software testing”, is a more costly part of the software development process that usually accounts for about 50% of the R&D budget of software development organizations.
Software testing relies on so-called “test cases” or more simply “tests”. To be efficient, tests should be generated in a relevant manner. For example, tests may be generated on the basis of information acquired from analyzing a program. Automating test generation from program analysis can roughly be partitioned into two groups: static versus dynamic test generation. Static test generation consists of analyzing a program statically to attempt to compute input values to drive its executions along specific program paths. In contrast, dynamic test generation consists in executing a program, typically starting with some random inputs, while simultaneously performing a symbolic execution to collect symbolic constraints on inputs obtained from predicates in branch statements along the execution, and then using a constraint solver to infer variants of the previous inputs in order to steer program executions along alternative program paths. Since dynamic test generation extends static test generation with additional runtime information, it can be more powerful.
While aspects of scalability of dynamic test generation have been recently addressed, significant issues exist as to how to dynamically check many properties simultaneously, thoroughly and efficiently, to maximize the chances of finding bugs during an automated testing session.
Traditional runtime checking tools (e.g., Purify, Valgrind and AppVerifier) check a single program execution against a set of properties (such as the absence of buffer overflows, uninitialized variables or memory leaks). Such techniques are referred to herein as traditional passive runtime property checking. As an example, consider the program: int divide(int n, int d){// n and d are inputs return (n/d); // division-by-zero error if d==0}. The program “divide” takes two integers n and d as inputs and computes their division. If the denominator d is zero, an error occurs. To catch this error, a traditional runtime checker for division-by zero would simply check whether a concrete value of d satisfies (d==0) just before the division is performed for a specific execution run, but it would not provide any insight or guarantee concerning other executions. Further, testing this program with random values for n and d is unlikely to detect the error, as d has only one chance out of 2=to be zero if d is a 32-bit integer. Static (and even dynamic) test generation techniques that attempt to cover specific or all feasible paths in a program will also likely miss the error since the program has a single program path which is covered no matter what inputs are used.
While an attempt at checking properties at runtime on a dynamic symbolic execution of a program has been reported, such an approach is likely to return false alarms whenever symbolic execution is imprecise, which is often the case in practice.
Various exemplary methods, devices, systems, etc., are described herein pertain to active property checking. Such techniques can extend runtime checking by checking whether the property is satisfied by all program executions that follow the same program path.